es:ES, P:(E), p:(e:E. Dec(P(e))), Q, R:(EE), A, B:Type, Ia:AbsInterface(A),
Ib:AbsInterface(B), f:(E(Ia)B), g:(E(Ib)E).
(e:E. ((e  Ib))  P(e))  g glues Ia:Q f (Ib|p):R  g glues Ia:Q f Ib:R 

latex

Definitions

t  T, let x,y = A in B(x;y), E, x:AB(x), x:A. B(x), f(a), x(s), x.A(x), x:A  B(x), b, ES, A, Dec(P), Type, x. t(x), EState(T), Id, , pred!(e;e'), SWellFounded(R(x;y)), loc(e), <a, b>, P  Q, constant_function(f;A;B), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, P & Q, Top, , e < e', r  s, val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), , Unit, left + right, Msg(M), type List, IdLnk, EOrderAxioms(E; pred?; info), EqDecider(T), E(X), {x:A| B(x)} , t.1, True, T, S  T, suptype(S; T), g glues Ia:Qa f Ib:Rb, {I}, X(e), Inj(A;B;f), f is Q-R-pre-preserving on P, Q = f== P, , (I|p), AbsInterface(A), s = t, e  X, SqStable(P)

Lemmas

subtype rel weakening, ext-eq weakening, sq stable subtype rel, es-interface-predicate wf, assert wf, es-is-interface wf, es-interface-restrict-trivial, weak-antecedent-surjection wf, Q-R-pre-preserving wf, inject wf, es-interface-val wf, Q-R-glues wf, es-interface-restrict wf, subtype rel function, es-E-interface wf, val-axiom wf, constant function wf, es-E-interface-restrict